\begin{tabbing}
$\forall$\=$T$:Type\{i\}, $L$:($T$ List), $R$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$)\} $\rightarrow$es\_realizer\{i:l\}),\+
\\[0ex]$P$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$)\} $\rightarrow$event\_system\{i:l\}$\rightarrow$prop\{i':l\}).
\-\\[0ex]($\forall$$x$,$y$:$T$. decidable(($x$ = $y$)))
\\[0ex]$\Rightarrow$ l\_all($L$; $T$; $x$.R{-}realizes\{i:l\}($R$($x$); ${\it es}$.$P$($x$,${\it es}$)))
\\[0ex]$\Rightarrow$ l\_all($L$; $T$; $x$.l\_all($L$; $T$; $y$.(($\neg$($x$ = $y$ $\in$ $T$)) $\Rightarrow$ R{-}compat\{i:l\}($R$($x$); $R$($y$)))))
\\[0ex]$\Rightarrow$ R{-}realizes\=\{i:l\}\+
\\[0ex](Rall($L$; $x$.$R$($x$)); ${\it es}$.l\_all($L$; $T$; $x$.$P$($x$,${\it es}$)))
\-
\end{tabbing}